Problem:
 top(sent(x)) -> top(check(rest(x)))
 rest(nil()) -> sent(nil())
 rest(cons(x,y)) -> sent(y)
 check(sent(x)) -> sent(check(x))
 check(rest(x)) -> rest(check(x))
 check(cons(x,y)) -> cons(check(x),y)
 check(cons(x,y)) -> cons(x,check(y))
 check(cons(x,y)) -> cons(x,y)

Proof:
 Complexity Transformation Processor:
  strict:
   top(sent(x)) -> top(check(rest(x)))
   rest(nil()) -> sent(nil())
   rest(cons(x,y)) -> sent(y)
   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   check(cons(x,y)) -> cons(check(x),y)
   check(cons(x,y)) -> cons(x,check(y))
   check(cons(x,y)) -> cons(x,y)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [cons](x0, x1) = x0 + x1,
     
     [nil] = 0,
     
     [check](x0) = x0 + 9,
     
     [rest](x0) = x0,
     
     [top](x0) = x0 + 127,
     
     [sent](x0) = x0
    orientation:
     top(sent(x)) = x + 127 >= x + 136 = top(check(rest(x)))
     
     rest(nil()) = 0 >= 0 = sent(nil())
     
     rest(cons(x,y)) = x + y >= y = sent(y)
     
     check(sent(x)) = x + 9 >= x + 9 = sent(check(x))
     
     check(rest(x)) = x + 9 >= x + 9 = rest(check(x))
     
     check(cons(x,y)) = x + y + 9 >= x + y + 9 = cons(check(x),y)
     
     check(cons(x,y)) = x + y + 9 >= x + y + 9 = cons(x,check(y))
     
     check(cons(x,y)) = x + y + 9 >= x + y = cons(x,y)
    problem:
     strict:
      top(sent(x)) -> top(check(rest(x)))
      rest(nil()) -> sent(nil())
      rest(cons(x,y)) -> sent(y)
      check(sent(x)) -> sent(check(x))
      check(rest(x)) -> rest(check(x))
      check(cons(x,y)) -> cons(check(x),y)
      check(cons(x,y)) -> cons(x,check(y))
     weak:
      check(cons(x,y)) -> cons(x,y)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [cons](x0, x1) = x0 + x1,
       
       [nil] = 0,
       
       [check](x0) = x0,
       
       [rest](x0) = x0,
       
       [top](x0) = x0 + 6,
       
       [sent](x0) = x0 + 2
      orientation:
       top(sent(x)) = x + 8 >= x + 6 = top(check(rest(x)))
       
       rest(nil()) = 0 >= 2 = sent(nil())
       
       rest(cons(x,y)) = x + y >= y + 2 = sent(y)
       
       check(sent(x)) = x + 2 >= x + 2 = sent(check(x))
       
       check(rest(x)) = x >= x = rest(check(x))
       
       check(cons(x,y)) = x + y >= x + y = cons(check(x),y)
       
       check(cons(x,y)) = x + y >= x + y = cons(x,check(y))
       
       check(cons(x,y)) = x + y >= x + y = cons(x,y)
      problem:
       strict:
        rest(nil()) -> sent(nil())
        rest(cons(x,y)) -> sent(y)
        check(sent(x)) -> sent(check(x))
        check(rest(x)) -> rest(check(x))
        check(cons(x,y)) -> cons(check(x),y)
        check(cons(x,y)) -> cons(x,check(y))
       weak:
        top(sent(x)) -> top(check(rest(x)))
        check(cons(x,y)) -> cons(x,y)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [cons](x0, x1) = x0 + x1 + 6,
         
         [nil] = 0,
         
         [check](x0) = x0,
         
         [rest](x0) = x0,
         
         [top](x0) = x0 + 8,
         
         [sent](x0) = x0 + 4
        orientation:
         rest(nil()) = 0 >= 4 = sent(nil())
         
         rest(cons(x,y)) = x + y + 6 >= y + 4 = sent(y)
         
         check(sent(x)) = x + 4 >= x + 4 = sent(check(x))
         
         check(rest(x)) = x >= x = rest(check(x))
         
         check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(check(x),y)
         
         check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(x,check(y))
         
         top(sent(x)) = x + 12 >= x + 8 = top(check(rest(x)))
         
         check(cons(x,y)) = x + y + 6 >= x + y + 6 = cons(x,y)
        problem:
         strict:
          rest(nil()) -> sent(nil())
          check(sent(x)) -> sent(check(x))
          check(rest(x)) -> rest(check(x))
          check(cons(x,y)) -> cons(check(x),y)
          check(cons(x,y)) -> cons(x,check(y))
         weak:
          rest(cons(x,y)) -> sent(y)
          top(sent(x)) -> top(check(rest(x)))
          check(cons(x,y)) -> cons(x,y)
        Splitting Processor:
         strict:
          check(cons(x,y)) -> cons(x,check(y))
         weak:
          rest(cons(x,y)) -> sent(y)
          top(sent(x)) -> top(check(rest(x)))
          check(cons(x,y)) -> cons(x,y)
          rest(nil()) -> sent(nil())
          check(sent(x)) -> sent(check(x))
          check(rest(x)) -> rest(check(x))
          check(cons(x,y)) -> cons(check(x),y)
         Matrix Interpretation Processor:
          dimension: 4
          max_matrix:
           [1 1 1 1]
           [0 1 0 0]
           [0 0 0 0]
           [0 0 0 0]
           interpretation:
                             [1 0 0 1]     [1 1 1 0]     [1]
                             [0 1 0 0]     [0 1 0 0]     [1]
            [cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
                             [0 0 0 0]     [0 0 0 0]     [0],
            
                    [0]
                    [0]
            [nil] = [0]
                    [0],
            
                          [1 1 0 0]  
                          [0 1 0 0]  
            [check](x0) = [0 0 0 0]x0
                          [0 0 0 0]  ,
            
                         [1 0 0 0]  
                         [0 1 0 0]  
            [rest](x0) = [0 0 0 0]x0
                         [0 0 0 0]  ,
            
                        [1 1 0 0]     [0]
                        [0 0 0 0]     [0]
            [top](x0) = [0 0 0 0]x0 + [0]
                        [0 0 0 0]     [1],
            
                         [1 1 1 0]  
                         [0 1 0 0]  
            [sent](x0) = [0 0 0 0]x0
                         [0 0 0 0]  
           orientation:
                          [0]    [0]              
                          [0]    [0]              
            rest(nil()) = [0] >= [0] = sent(nil())
                          [0]    [0]              
            
                             [1 2 1 0]     [1 2 0 0]                  
                             [0 1 0 0]     [0 1 0 0]                  
            check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
                             [0 0 0 0]     [0 0 0 0]                  
            
                             [1 1 0 0]     [1 1 0 0]                  
                             [0 1 0 0]     [0 1 0 0]                  
            check(rest(x)) = [0 0 0 0]x >= [0 0 0 0]x = rest(check(x))
                             [0 0 0 0]     [0 0 0 0]                  
            
                               [1 1 0 1]    [1 2 1 0]    [2]    [1 1 0 0]    [1 1 1 0]    [1]                   
                               [0 1 0 0]    [0 1 0 0]    [1]    [0 1 0 0]    [0 1 0 0]    [1]                   
            check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(check(x),y)
                               [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
            
                               [1 1 0 1]    [1 2 1 0]    [2]    [1 0 0 1]    [1 2 0 0]    [1]                   
                               [0 1 0 0]    [0 1 0 0]    [1]    [0 1 0 0]    [0 1 0 0]    [1]                   
            check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y))
                               [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
            
                              [1 0 0 1]    [1 1 1 0]    [1]    [1 1 1 0]           
                              [0 1 0 0]    [0 1 0 0]    [1]    [0 1 0 0]           
            rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y = sent(y)
                              [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]           
            
                           [1 2 1 0]    [0]    [1 2 0 0]    [0]                      
                           [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
            top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
                           [0 0 0 0]    [1]    [0 0 0 0]    [1]                      
            
                               [1 1 0 1]    [1 2 1 0]    [2]    [1 0 0 1]    [1 1 1 0]    [1]            
                               [0 1 0 0]    [0 1 0 0]    [1]    [0 1 0 0]    [0 1 0 0]    [1]            
            check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,y)
                               [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]            
           problem:
            strict:
             rest(nil()) -> sent(nil())
             check(sent(x)) -> sent(check(x))
             check(rest(x)) -> rest(check(x))
            weak:
             check(cons(x,y)) -> cons(check(x),y)
             check(cons(x,y)) -> cons(x,check(y))
             rest(cons(x,y)) -> sent(y)
             top(sent(x)) -> top(check(rest(x)))
             check(cons(x,y)) -> cons(x,y)
           Splitting Processor:
            strict:
             rest(nil()) -> sent(nil())
            weak:
             check(cons(x,y)) -> cons(check(x),y)
             check(cons(x,y)) -> cons(x,check(y))
             rest(cons(x,y)) -> sent(y)
             top(sent(x)) -> top(check(rest(x)))
             check(cons(x,y)) -> cons(x,y)
             check(sent(x)) -> sent(check(x))
             check(rest(x)) -> rest(check(x))
            Splitting Processor:
             strict:
              check(sent(x)) -> sent(check(x))
             weak:
              rest(nil()) -> sent(nil())
              check(cons(x,y)) -> cons(check(x),y)
              check(cons(x,y)) -> cons(x,check(y))
              rest(cons(x,y)) -> sent(y)
              top(sent(x)) -> top(check(rest(x)))
              check(cons(x,y)) -> cons(x,y)
              check(rest(x)) -> rest(check(x))
             Matrix Interpretation Processor:
              dimension: 4
              max_matrix:
               [1 1 1 1]
               [0 0 1 1]
               [0 0 1 1]
               [0 0 0 0]
               interpretation:
                                 [1 0 0 0]     [1 0 1 0]     [1]
                                 [0 0 1 0]     [0 0 0 1]     [0]
                [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0]
                                 [0 0 0 0]     [0 0 0 0]     [0],
                
                        [0]
                        [0]
                [nil] = [0]
                        [1],
                
                              [1 0 1 0]  
                              [0 0 1 0]  
                [check](x0) = [0 0 1 0]x0
                              [0 0 0 0]  ,
                
                             [1 0 0 1]     [0]
                             [0 0 1 1]     [1]
                [rest](x0) = [0 0 1 0]x0 + [1]
                             [0 0 0 0]     [0],
                
                            [1 1 0 0]     [0]
                            [0 0 1 0]     [1]
                [top](x0) = [0 0 1 0]x0 + [0]
                            [0 0 0 0]     [0],
                
                             [1 0 1 0]     [1]
                             [0 0 1 1]     [1]
                [sent](x0) = [0 0 1 0]x0 + [1]
                             [0 0 0 0]     [0]
               orientation:
                                 [1 0 2 0]    [2]    [1 0 2 0]    [1]                 
                                 [0 0 1 0]    [1]    [0 0 1 0]    [1]                 
                check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x))
                                 [0 0 0 0]    [0]    [0 0 0 0]    [0]                 
                
                              [1]    [1]              
                              [2]    [2]              
                rest(nil()) = [1] >= [1] = sent(nil())
                              [0]    [0]              
                
                                   [1 0 1 0]    [1 0 2 1]    [1]    [1 0 1 0]    [1 0 1 0]    [1]                   
                                   [0 0 1 0]    [0 0 1 1]    [0]    [0 0 1 0]    [0 0 0 1]    [0]                   
                check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y)
                                   [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
                
                                   [1 0 1 0]    [1 0 2 1]    [1]    [1 0 0 0]    [1 0 2 0]    [1]                   
                                   [0 0 1 0]    [0 0 1 1]    [0]    [0 0 1 0]    [0 0 0 0]    [0]                   
                check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y))
                                   [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
                
                                  [1 0 0 0]    [1 0 1 0]    [1]    [1 0 1 0]    [1]          
                                  [0 0 1 0]    [0 0 1 1]    [1]    [0 0 1 1]    [1]          
                rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y)
                                  [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0]          
                
                               [1 0 2 1]    [2]    [1 0 2 1]    [2]                      
                               [0 0 1 0]    [2]    [0 0 1 0]    [2]                      
                top(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = top(check(rest(x)))
                               [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
                
                                   [1 0 1 0]    [1 0 2 1]    [1]    [1 0 0 0]    [1 0 1 0]    [1]            
                                   [0 0 1 0]    [0 0 1 1]    [0]    [0 0 1 0]    [0 0 0 1]    [0]            
                check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y)
                                   [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]            
                
                                 [1 0 1 1]    [1]    [1 0 1 0]    [0]                 
                                 [0 0 1 0]    [1]    [0 0 1 0]    [1]                 
                check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x))
                                 [0 0 0 0]    [0]    [0 0 0 0]    [0]                 
               problem:
                strict:
                 
                weak:
                 check(sent(x)) -> sent(check(x))
                 rest(nil()) -> sent(nil())
                 check(cons(x,y)) -> cons(check(x),y)
                 check(cons(x,y)) -> cons(x,check(y))
                 rest(cons(x,y)) -> sent(y)
                 top(sent(x)) -> top(check(rest(x)))
                 check(cons(x,y)) -> cons(x,y)
                 check(rest(x)) -> rest(check(x))
               Qed
              
              strict:
               check(rest(x)) -> rest(check(x))
              weak:
               check(sent(x)) -> sent(check(x))
               rest(nil()) -> sent(nil())
               check(cons(x,y)) -> cons(check(x),y)
               check(cons(x,y)) -> cons(x,check(y))
               rest(cons(x,y)) -> sent(y)
               top(sent(x)) -> top(check(rest(x)))
               check(cons(x,y)) -> cons(x,y)
              Matrix Interpretation Processor:
               dimension: 4
               max_matrix:
                [1 1 1 1]
                [0 0 1 1]
                [0 0 1 1]
                [0 0 0 0]
                interpretation:
                                  [1 0 0 0]     [1 0 1 0]     [1]
                                  [0 0 0 0]     [0 0 1 0]     [0]
                 [cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0]
                                  [0 0 0 0]     [0 0 0 0]     [0],
                 
                         [0]
                         [0]
                 [nil] = [0]
                         [1],
                 
                               [1 0 1 0]  
                               [0 0 1 0]  
                 [check](x0) = [0 0 1 0]x0
                               [0 0 0 0]  ,
                 
                              [1 0 0 1]     [0]
                              [0 0 1 1]     [1]
                 [rest](x0) = [0 0 1 0]x0 + [1]
                              [0 0 0 0]     [0],
                 
                             [1 1 0 0]  
                             [0 0 0 0]  
                 [top](x0) = [0 0 0 0]x0
                             [0 0 0 0]  ,
                 
                              [1 0 1 0]     [1]
                              [0 0 1 1]     [1]
                 [sent](x0) = [0 0 1 0]x0 + [1]
                              [0 0 0 0]     [0]
                orientation:
                                  [1 0 1 1]    [1]    [1 0 1 0]    [0]                 
                                  [0 0 1 0]    [1]    [0 0 1 0]    [1]                 
                 check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x))
                                  [0 0 0 0]    [0]    [0 0 0 0]    [0]                 
                 
                                  [1 0 2 0]    [2]    [1 0 2 0]    [1]                 
                                  [0 0 1 0]    [1]    [0 0 1 0]    [1]                 
                 check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x))
                                  [0 0 0 0]    [0]    [0 0 0 0]    [0]                 
                 
                               [1]    [1]              
                               [2]    [2]              
                 rest(nil()) = [1] >= [1] = sent(nil())
                               [0]    [0]              
                 
                                    [1 0 1 0]    [1 0 2 1]    [1]    [1 0 1 0]    [1 0 1 0]    [1]                   
                                    [0 0 1 0]    [0 0 1 1]    [0]    [0 0 0 0]    [0 0 1 0]    [0]                   
                 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y)
                                    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
                 
                                    [1 0 1 0]    [1 0 2 1]    [1]    [1 0 0 0]    [1 0 2 0]    [1]                   
                                    [0 0 1 0]    [0 0 1 1]    [0]    [0 0 0 0]    [0 0 1 0]    [0]                   
                 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y))
                                    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]                   
                 
                                   [1 0 0 0]    [1 0 1 0]    [1]    [1 0 1 0]    [1]          
                                   [0 0 1 0]    [0 0 1 1]    [1]    [0 0 1 1]    [1]          
                 rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y)
                                   [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0]          
                 
                                [1 0 2 1]    [2]    [1 0 2 1]    [2]                      
                                [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
                 top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
                                [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
                 
                                    [1 0 1 0]    [1 0 2 1]    [1]    [1 0 0 0]    [1 0 1 0]    [1]            
                                    [0 0 1 0]    [0 0 1 1]    [0]    [0 0 0 0]    [0 0 1 0]    [0]            
                 check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y)
                                    [0 0 0 0]    [0 0 0 0]    [0]    [0 0 0 0]    [0 0 0 0]    [0]            
                problem:
                 strict:
                  
                 weak:
                  check(rest(x)) -> rest(check(x))
                  check(sent(x)) -> sent(check(x))
                  rest(nil()) -> sent(nil())
                  check(cons(x,y)) -> cons(check(x),y)
                  check(cons(x,y)) -> cons(x,check(y))
                  rest(cons(x,y)) -> sent(y)
                  top(sent(x)) -> top(check(rest(x)))
                  check(cons(x,y)) -> cons(x,y)
                Qed
             
             strict:
              check(sent(x)) -> sent(check(x))
              check(rest(x)) -> rest(check(x))
             weak:
              rest(nil()) -> sent(nil())
              check(cons(x,y)) -> cons(check(x),y)
              check(cons(x,y)) -> cons(x,check(y))
              rest(cons(x,y)) -> sent(y)
              top(sent(x)) -> top(check(rest(x)))
              check(cons(x,y)) -> cons(x,y)
             Matrix Interpretation Processor:
              dimension: 4
              max_matrix:
               [1 1 1 1]
               [0 0 1 1]
               [0 0 1 1]
               [0 0 0 0]
               interpretation:
                                 [1 0 0 0]     [1 0 1 1]  
                                 [0 0 0 0]     [0 0 0 0]  
                [cons](x0, x1) = [0 0 0 0]x0 + [0 0 1 1]x1
                                 [0 0 0 0]     [0 0 0 0]  ,
                
                        [0]
                        [0]
                [nil] = [0]
                        [1],
                
                              [1 0 0 0]  
                              [0 0 1 0]  
                [check](x0) = [0 0 1 0]x0
                              [0 0 0 0]  ,
                
                             [1 0 0 1]  
                             [0 0 1 1]  
                [rest](x0) = [0 0 1 0]x0
                             [0 0 0 0]  ,
                
                            [1 1 0 0]     [0]
                            [0 0 0 0]     [0]
                [top](x0) = [0 0 0 0]x0 + [1]
                            [0 0 0 0]     [0],
                
                             [1 0 1 0]  
                             [0 0 0 1]  
                [sent](x0) = [0 0 0 0]x0
                             [0 0 0 0]  
               orientation:
                              [1]    [0]              
                              [1]    [1]              
                rest(nil()) = [0] >= [0] = sent(nil())
                              [0]    [0]              
                
                                   [1 0 0 0]    [1 0 1 1]     [1 0 0 0]    [1 0 1 1]                    
                                   [0 0 0 0]    [0 0 1 1]     [0 0 0 0]    [0 0 0 0]                    
                check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 1]y = cons(check(x),y)
                                   [0 0 0 0]    [0 0 0 0]     [0 0 0 0]    [0 0 0 0]                    
                
                                   [1 0 0 0]    [1 0 1 1]     [1 0 0 0]    [1 0 1 0]                    
                                   [0 0 0 0]    [0 0 1 1]     [0 0 0 0]    [0 0 0 0]                    
                check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 0]y = cons(x,check(y))
                                   [0 0 0 0]    [0 0 0 0]     [0 0 0 0]    [0 0 0 0]                    
                
                                  [1 0 0 0]    [1 0 1 1]     [1 0 1 0]           
                                  [0 0 0 0]    [0 0 1 1]     [0 0 0 1]           
                rest(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]y = sent(y)
                                  [0 0 0 0]    [0 0 0 0]     [0 0 0 0]           
                
                               [1 0 1 1]    [0]    [1 0 1 1]    [0]                      
                               [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
                top(sent(x)) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = top(check(rest(x)))
                               [0 0 0 0]    [0]    [0 0 0 0]    [0]                      
                
                                   [1 0 0 0]    [1 0 1 1]     [1 0 0 0]    [1 0 1 1]             
                                   [0 0 0 0]    [0 0 1 1]     [0 0 0 0]    [0 0 0 0]             
                check(cons(x,y)) = [0 0 0 0]x + [0 0 1 1]y >= [0 0 0 0]x + [0 0 1 1]y = cons(x,y)
                                   [0 0 0 0]    [0 0 0 0]     [0 0 0 0]    [0 0 0 0]             
                
                                 [1 0 1 0]     [1 0 1 0]                  
                                 [0 0 0 0]     [0 0 0 0]                  
                check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
                                 [0 0 0 0]     [0 0 0 0]                  
                
                                 [1 0 0 1]     [1 0 0 0]                  
                                 [0 0 1 0]     [0 0 1 0]                  
                check(rest(x)) = [0 0 1 0]x >= [0 0 1 0]x = rest(check(x))
                                 [0 0 0 0]     [0 0 0 0]                  
               problem:
                strict:
                 
                weak:
                 rest(nil()) -> sent(nil())
                 check(cons(x,y)) -> cons(check(x),y)
                 check(cons(x,y)) -> cons(x,check(y))
                 rest(cons(x,y)) -> sent(y)
                 top(sent(x)) -> top(check(rest(x)))
                 check(cons(x,y)) -> cons(x,y)
                 check(sent(x)) -> sent(check(x))
                 check(rest(x)) -> rest(check(x))
               Qed
            
            strict:
             rest(nil()) -> sent(nil())
             check(sent(x)) -> sent(check(x))
             check(rest(x)) -> rest(check(x))
             check(cons(x,y)) -> cons(check(x),y)
            weak:
             check(cons(x,y)) -> cons(x,check(y))
             rest(cons(x,y)) -> sent(y)
             top(sent(x)) -> top(check(rest(x)))
             check(cons(x,y)) -> cons(x,y)
            Matrix Interpretation Processor:
             dimension: 3
             max_matrix:
              [1 0 1]
              [0 0 0]
              [0 0 1]
              interpretation:
                                [1 0 0]     [1 0 1]     [0]
               [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                                [0 0 1]     [0 0 1]     [1],
               
                       [1]
               [nil] = [0]
                       [0],
               
                             [1 0 1]     [0]
               [check](x0) = [0 0 0]x0 + [1]
                             [0 0 1]     [0],
               
                            [1 0 0]     [0]
               [rest](x0) = [0 0 0]x0 + [1]
                            [0 0 1]     [0],
               
                           [1 0 0]  
               [top](x0) = [0 0 0]x0
                           [0 0 1]  ,
               
                            [1 0 1]     [0]
               [sent](x0) = [0 0 0]x0 + [1]
                            [0 0 1]     [0]
              orientation:
                                  [1 0 1]    [1 0 2]    [1]    [1 0 0]    [1 0 2]    [0]                   
               check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,check(y))
                                  [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0 0 1]    [1]                   
               
                                 [1 0 0]    [1 0 1]    [0]    [1 0 1]    [0]          
               rest(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]y + [1] = sent(y)
                                 [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0]          
               
                              [1 0 1]     [1 0 1]                       
               top(sent(x)) = [0 0 0]x >= [0 0 0]x = top(check(rest(x)))
                              [0 0 1]     [0 0 1]                       
               
                                  [1 0 1]    [1 0 2]    [1]    [1 0 0]    [1 0 1]    [0]            
               check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,y)
                                  [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0 0 1]    [1]            
               
                             [1]    [1]              
               rest(nil()) = [1] >= [1] = sent(nil())
                             [0]    [0]              
               
                                [1 0 2]    [0]    [1 0 2]    [0]                 
               check(sent(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = sent(check(x))
                                [0 0 1]    [0]    [0 0 1]    [0]                 
               
                                [1 0 1]    [0]    [1 0 1]    [0]                 
               check(rest(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = rest(check(x))
                                [0 0 1]    [0]    [0 0 1]    [0]                 
               
                                  [1 0 1]    [1 0 2]    [1]    [1 0 1]    [1 0 1]    [0]                   
               check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [0] = cons(check(x),y)
                                  [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0 0 1]    [1]                   
              problem:
               strict:
                
               weak:
                check(cons(x,y)) -> cons(x,check(y))
                rest(cons(x,y)) -> sent(y)
                top(sent(x)) -> top(check(rest(x)))
                check(cons(x,y)) -> cons(x,y)
                rest(nil()) -> sent(nil())
                check(sent(x)) -> sent(check(x))
                check(rest(x)) -> rest(check(x))
                check(cons(x,y)) -> cons(check(x),y)
              Qed